i:Id, ds:x:Id fp Type, x:Id, k:Knd, T:Type, test:(State(ds)T), es:ES.
recognizer(es;i;ds;x;k;T;test)   

latex

Definitions	Top, P  Q, {T}, P  Q, SQType(T), x. t(x), x:A. B(x), P  Q, P & Q, A c B, recognizer(es;i;ds;x;k;T;test), , t  T, x:A. B(x), x(s), @i(x:T)
Lemmas	Knd sq, es-valtype-kindtype, fpf wf, Id wf, Knd wf, bool wf, decl-state wf, event system wf, es-initially wf, es-le-loc, Id sq, es-vartype wf, es-after wf, assert wf, iff wf, es-loc wf, alle-at wf